По просьбам трудящихся: пример моей модели на uppaal.

P.S. проверять количество состояний нужно с помощью бинарника verifyta, например:
./verifyta -u 421_Guskov_2.xml

P.S.S. проверяемое свойство нужно задать во вкладке верификатора uppaal так, чтобы верификатор прошёл все состояния, например:
A[] M2.y >= 0